\begin{tabbing}
d{-}world\=\{i:l\}\+
\\[0ex]($D$; $v$; ${\it sched}$; ${\it dec}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$($\lambda$$i$,$x$. d{-}m($D$; $i$).ds($x$))\+
\\[0ex]$,\,$($\lambda$$i$,$a$. d{-}m($D$; $i$).da(locl($a$)))
\\[0ex]$,\,$($\lambda$$l$,${\it tg}$. d{-}m($D$; source($l$)).dout($l$,${\it tg}$))
\\[0ex]$,\,$($\lambda$$i$,$t$. \=if $t$=$_{2}$0$\rightarrow$ $\lambda$$x$.d{-}m($D$; $i$).init($x$)?$v$($i$,$x$)\+
\\[0ex]else 1of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$$-$1,$i$)) fi)
\-\\[0ex]$,\,$($\lambda$$i$,$t$. 1of(2of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$,$i$))))
\\[0ex]$,\,$($\lambda$$i$,$t$. 2of(2of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$,$i$))))
\\[0ex]$,\,$($\lambda$$i$.d{-}machine($i$;d{-}m($D$; $i$);${\it dec}$($i$)))
\\[0ex]$,\,$$\cdot$$\rangle$
\-
\end{tabbing}